(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun d () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun r () Real)
(declare-fun g () Real)
(declare-fun s () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert (not (exists ((j Real)) (let ((?k (>= r 0))(?l (<= r (/ 0 0)))(?t (/ (* r r) (* 2 (- (- b (- 680.2932226634903)) o))))(?m (* (/ 1 2) (+ (* (* 2 f) r) 0)))) (=> (and (and (and (and (and (and (and (and (=> (and (<= 0 j f)) (and (<= j g))) (>= f 0)) (= (/ c d) s)) (> (/ a n) (+ (+ s ?t) (* (+ (/ q e) 1) (+ (* (/ q 2) (* g g)) (* g r)))))) ?k) ?l) (< (/ a n) i)) (> (- (- b (- 680.2932226634903)) o) 0)) (>= q 0)) (or (or (= h 2) (< p ?m)) (> (/ a n) (+ ?m ?t))))))))
(assert (= a (* n p)))
(assert (= p (/ a n)))
(assert (= b (+ (+ e o) (- 680.2932226634903))))
(assert (= d (/ c p)))
(assert (= p (/ c d)))
(check-sat)
